COMMENT ⊗   VALID 00007 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00007 00003	.bb "#. The Functional Equation and the Minimization Schema"
C00016 00004	.bb "#. Proof Methods as Axiom Schemata"
C00020 00005	.bb "#. Representability in Lisp"
C00031 00006	.bb "#. Discussion"
C00035 00007	.skip 1
C00036 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source;
.CB draft

.CB REPRESENTATION OF RECURSIVE PROGRAMS IN FIRST ORDER LOGIC


	By %2recursive program%1 we mean a partial function defined by
an expression of the form

!!i1:	%2f(x) ← %At%2[f](x)%1,

where %At%2[f]%1 is a continuous functional like

!!i0:	%At%2 = λf.λx.(qif p(x) qthen x qelse f(h(x)))%1

which corresponds to the Lisp-like conditional expression function definition

!!i00:	%2f(x) ← qif p(x) qthen x qelse f(h(x))%1.

Often we will omit parentheses around the arguments of unary functions
and predicates so that the above definition may also be written

	%2f x ← qif p x qthen x qelse f h x%1.

%2Recursive programs%1 compute the same partial functions
as Turing machines or general recursive functions
when the domain is the set of integers and the successor function and equality
are available.  However,
recursive programs can be given over arbitrary domains with arbitrary
sets of base functions.  We will be especially concerned with
the domain of Lisp S-expressions and the functions definable from ⊗car, 
⊗cdr, ⊗cons and the predicate ⊗atoms and equality.
Programs involving the mutual recursion of several
functions can be treated similarly,
and we shall take the least fixed point interpretation of the definitions.
We rely on (Manna 1974) and (Manna, Ness, and Vuillemin 1973) for background.

	There are many reasons for wanting to represent recursive
programs in first order logic.  First, theorem provers and proof-checkers
are well-developed for first order logic.  Second, set theory is
formulated in first order logic and is the main available tool for
formulating mathematical theories relevant to proving assertions about
computer programs.  Finally, since first order logic is complete, any
necessary incompleteness takes the form of incomplete axioms systems
rather than incomplete logic, and extensions to mitigate the
incompleteness can be accomplished by extending the axioms rather than by
extending the logic.

	This note describes two new approaches to representing Lisp-recursive
definitions in first order logic and examples of their use in proving
assertions about the resulting functions.

	The first approach involves representing any Lisp-recursive
definition over an abstract domain by a first order %2functional equation%1
and a first order %2minimization schema%1, and the second involves
characterizing Lisp functions by first order sentences involving either
%2pair-lists%1 of (argument.value) pairs or %2traces%1 of their
computation.  The relations between the two approaches are still
unexplored.
.skip 2
.item←0
.bb "#. The Functional Equation and the Minimization Schema"

	The first method parallels Peano arithmetic in the following way:
Corresponding to each recursive definition is a sentence of first order
logic called its %2functional equation%1 and a sentence schema of first
order logic called its %2minimization schema%1.  These two formulas
"attempt" to characterize the function.  Non-trivial recursively defined
functions cannot be fully characterized by these formulas, because
non-standard solutions of the equation and schema are possible.  However,
these non-standard solutions seem to resemble the non-standard sum and
product functions of non-standard arithmetic, and satisfy almost all the
same formulas as the standard functions.  Therefore, it seems likely that
the first order theory will be adequate to prove almost any assertions
about the program that will normally arise just as Peano arithmetic
is adequate to prove all the ordinary theorems.
In some contrast to Peano arithmetic, it looks like the proofs will
be of reasonable length in many interesting cases even without using
a set-theoretic formalization.

	We begin with an example.  Consider the recursive definition

!!a1:	%2f%41%2 x ← qif p x qthen h x qelse g1 f%41%2 g2 x%1,

where ⊗p is a known total predicate on the domain of integers,
and ⊗h, ⊗g1, and ⊗g2 are known
integer-valued total functions on the integers.

	The %2functional equation%1 corresponding to ({eq a1}) is

!!a2:	%2∀x.(f%41%2 x = qif p x qthen h x qelse g1 f%41%2 g2 x)%1

with the following provisos:  First, the quantifier ⊗∀x ranges
over the domain of integers.  Second, %2f(x)%1 is not required
to be an integer; it will be an integer when the computation process
of ({eq a1}) terminates.  In fact, proving that it is an integer is our
way of proving termination.

	Regarded as a call-by-name computation rule, ({eq a1}) defines a
partial function which is also the least fixed point of the relevant
continuous functional as described in (Manna 1974).  Now we augment the
integers by an element %AW%1, give the function ⊗f the value %AW%1 for
those ⊗x for which ⊗f' is undefined.  Because of the existence of the
least fixed points, ({eq a2}) always admits this interpretation regardless
of the right hand side.  Therefore, we can write the equation
corresponding to ({eq a2}) for any recursive definition.  The following
examples are instructive:

	From

!!a3:	%2f%42%2 x ← f%42%2 x%1

we get the equation

!!a4:	%2∀x.(f%42%2 x = f%42%2 x)%1,

which is not very helpful, because it is satisfied by any function -
integer-valued or not.  From

!!a5:	%2f%43%2 x ← 1 + f%43%2 x%1

we get

!!a6:	%2∀x.(f%43%2 x = 1 + f%43%2 x)%1

which is not satisfied by any integer-valued function.  The properties of
addition that would make ({eq a6}) inconsistent if we insisted that %2f%43%2(x)%1
always be an integer, had better not be satisfied outside the integers
and are sufficient to show that %2f%43%2(x)%1 is not an integer, from which we
can conclude that the partial function defined by ({eq a5}) never
terminates.

	From

!!a7:	%2fact x ← qif x = 0 qthen 1 qelse x * fact(x-1)%1,

we get

!!a8:	%2∀x.(fact x ← qif x = 0 qthen 1 qelse x * fact(x-1))%1

where we are using conditional expressions to make terms in first
order logic.  From ({eq a8}) we can prove by mathematical induction
that ⊗fact(x) is always an integer, and the other customary properties
of the factorial function can then be proved by induction.

	When the recursive definition defines a total function, then
this function is characterized by the corresponding %2functional equation%1.
However, since the functional equation may have many solutions, the
minimal solution is not characterized in general.  We ⊗try to
characterize the minimal solution by the following %2minimization schema%1:

!!a9:	%2∀x.(isinteger(qif p x qthen h x qelse g1 %Af%2 g2 x) ⊃
%Af%2 x = qif p x qthen h x qelse g1 %Af%2 g2 x)
⊃ ∀x.(isinteger(f x) ⊃ f x = %Af%2 x)%1,

where %Af%1 is a function variable that may be replaced by an
arbitrary function symbol to get a first order sentence.  The schema
asserts that ⊗f is the least solution of the functional equation by
asserting that any partial function %Af%1 that extends its "right hand
side" is an extension of ⊗f.  This equation is a special case of

!!a10:	%Af%8 d %2F(%Af%2) ⊃ %Af%8 d %2Y(F)%1

in the notation of Scott (197?), but we want to stick to first order
logic.

	The schemata corresponding to ({eq a3}) and ({eq a5}) are

!!a11:	%2∀x.(isinteger %Af%2(x) ⊃ %Af%2(x) = %Af%2(x)) ⊃
∀x.(isinteger f%42%2(x) ⊃ f%42%2(x) = %Af%2(x))%1

and

!!a12:	%2∀x.(isinteger %Af%2(x) ⊃ %Af%2(x) = 1 + %Af%2(x)) ⊃
∀x.(isinteger f%43%2(x) ⊃ f%43%2(x) = %Af%2(x))%1.

.fill
	Since %Af%2(x) = %AW%1 is a solution of the left side of ({eq a11}),
%2f%42%2(x)%1 is never an integer; this could not be shown
without the schema.

	What we shall be able to prove with the schema depends on what
facilities we have for naming the %2comparison functions%1 that we
substitute into it.
.skip 2
.bb "#. Proof Methods as Axiom Schemata"

	Representing recursive definitions in first order logic permits
us to expresse well known methods for proving partial correctness
as axiom schemata of first order logic.

	For example, suppose we want to prove that if the input ⊗x of a
function ⊗f defined by

!!c1:	%2f x ← qif p x qthen x qelse f h x%1

satisfies %2P(x)%1, then if the function terminates, the output %2f(x)%1
will satisfy %Ay%2(f(x))%1.  We appeal to the following %2axiom schema of
inductive assertions%1:

!!c2:	%2∀x.(P(x) ⊃ q(x,x)) ∧ ∀x y.(q(x,y) ⊃ qif p x qthen %Ay%2(x,y)
qelse q(x,%8 %2h y))
.nofill
		⊃ ∀x.(P(x) ∧ inrange f x ⊃ %Ay%2(x,f x))%1

.fill
where %2inrange f x%1 is the assertion that %2f(x)%1 is in the nominal
range of the function definition, i.e. is an integer or an S-expression
as the case may be, and asserts that the computation terminates.
In order to use the schema, we must invent a suitable predicate %2q(x,y)%1,
and this is precisely the method of inductive assertions.
The schema is valid for all predicates %Af%1, %Ay%1, and %2q%1, and a
similar schema can be written for any collection of mutually recursive
definitions that is iterative.

	The method of %2subgoal induction%1 (Morris and Wegbreit 19xx) is
not limited to iterative definitions.  Thus it can be formulated for

!!c3:	%2f%41%2 x ← qif p x qthen h x qelse g1 f%41%2 g2 x%1

discussed in the previous section.
The schema is

!!c4:	%2∀x.(p x ⊃ q(x,h x)) ∧ ∀x z.(¬p(x) ∧ q(g2 x,z) ⊃ q(x,g1 z)) ∧
∀x.(P(x) ∧ q(x,z) ⊃ %Ay%2(x,z))
.nofill
		⊃ ∀x.(%Af%2(x) ∧ inrange(f(x)) ⊃ %Ay%2(x,f(x)))%1
.fill

	The possibility of expressing these methods as axiom schemata
depends on the fact that the predicate %2inrange%1 expresses termination.
The minimization schema itself is a consequence of subgoal induction.
We need only take %2P(x)_≡_%3true%1 and %Ay%2(x,y)_≡_q(x,y)_=_(y_=_%Af%2(x)%1.
.skip 2
.bb "#. Representability in Lisp"
%1
	The second approach to showing that facts about recursively
defined functions are expressible as first order sentences goes back
to Goedel (1931, 1934).

.turn on "α"
.eq←0
	In Peano arithmetic, a function ⊗f is called representable if there
is an arithmetic formula ⊗A with free variables ⊗x and ⊗y such
that

!!b1:	%2∀x_y.((y_=_f(x))_≡_A)%1,

where an arithmetic formula is built up from integer constants and
variables using only addition, multiplication and bounded quantification.
Goedel showed that all partial recursive functions
are representable.
The proof involves Goedel numbering possible computation sequences
and showing that the relation between sequences and their elements
and the steps of the computation are all representable.

	In Lisp the situation is simpler, because sequences
are Lisp data, and the relation between a sequence and its elements
is given by basic Lisp functions and by the %2subexpression relation%1
defined by

!!b2:	%2x subexp y ← (x = y) ∨ ¬qat y ∧ [x subexp qa y ∨ x subexp qd y]%1.

	According to the previous section, %2subexp%1 is characterized
by the sentence

!!b13:	%2∀x y.(x subexp y ≡ (x = y) ∨ ¬qat y ∧ [x subexp qa y ∨ x subexp qd y])%1.

There is also an axiom schema, but since ({eq b13}) is sufficient to
prove that %2x_subexp_y%1 is total, the schema seems to be redundant.

	Given %2subexp%1, all other Lisp functions can
be defined explicitly (i.e. without recursion)
by formulas of predicate logic.  While such definitions
may not be useful for computation, they may be useful for
proving assertions about Lisp functions.

	The first useful function is the %2sublist%1 predicate whose
recursive definition is

!!b3:	%2u sublist v ← (u = v) ∨ ¬qn v ∧ u sublist qd v%1

but which can be defined in terms of %2subexp%1 without recursion by

!!b4:	%2∀u v.(u sublist v ≡ u subexp v ∧ ∀x.(u subexp x ∧ x subexp v ⊃
qat x ∨ ¬(u subexp qa x)))%1.

This insures that in descending from ⊗v to ⊗u, we never go in the
qa-direction.

	Consider our favorite function ⊗alt defined by

!!b5:	%2alt u ← qif qn u ∨ qn qd u qthen u qelse qa u . alt qdd u%1.

We represent it by the formula

!!b6:	%2∀u v.(v = alt u ≡ ∃w.(u = qaa w ∧ v = qda w ∧ ∀w1.(w1 sublist w
⊃ qn w1 ∨ (qif qn qaa w1 ∨ qn qd qaa w1 qthen qn qd w1 ∧ qda w1 = qaa w1
qelse ¬qn qd w1 ∧ qaaqd w1 = qdd qaa w1 ∧ qda w1 = qaa w1 . qdaqd w1)))%1.

	The ⊗w whose existence is asserted is a list of pairs
%2(x . alt x)%1, and each ⊗x on the list is qdd of the preceding.
Thus in computing %2alt%1_(A_B_C_D_E)_=_(A_C_E), we have

!!b7:	%2w = %1(((A B C D E).(A C E)) ((C D E).(C E)) ((E).(E))).

The sentence ({eq b6}) mainly relates each sublist of this %2trace%1
of the computation with its successor.

	Suppose now that we have a collection %2α{f%41%2, ... ,f%4n%2α}%1
of functions defined by a mutual recursion.  A representation in
terms of a trace is somewhat tedious to write down but can be
done in a variety of straightforward ways.  In fact, we could give
a Lisp function to go from a collection of function definitions
to the representing sentences.

	The fact that representability requires only the %2subexp%1
relation tells us something about the model theory of Lisp.  Namely,
the non-standard models of Lisp are just the non-standard models of
this relation and the basic Lisp functions.  This situation should
be simpler than the situation with the integers and might even throw
some light on the structure of the non-standard models of the integers
since the integers can be represented as S-expressions.

.TURN OFF "α"
	Now we give a systematic way of representing recursively defined
functions by non-recursive sentences of first order logic that characterize
the function by %2pair-lists%1 whose members are (argument.value) pairs
for the function.
First, we define

!!d2:	%2 x εε w ≡ ∃w1.(w1 subexp w ∧ x = qaa w1)%1,

and

!!d3:	%2α(w,x) = qif qn assoc(x,w) qthen %AW%2 qelse qd assoc(x,w)%1.

Now suppose that ⊗f is given by

!!d1:	%2f = Y(F)%1

in Scottish.
We then define

!!d4:	%2∀w.[pairlist(w,F) ≡ ∀x.[x εε w ≡ α(w,x) = F(λz.α(w,z))(x)]]%1

from which follows

!!d5:	%2∀x y.[y = f(x) ≡ ∃w.[pairlist(w,F) ∧ y = α(w,x)]]%1.

	The functions ε, εε and α are all representable using %2subexp%1.
Sentences ({eq d4}) and ({eq d5}) are not first order in ⊗F, but for
any fixed ⊗F they become first order sentences.  Consider the
rather complicated recursive definition

!!d7:	%2f x ← qif p1 x qthen g1 x qelse qif p2(x,f h1 x) qthen g2 x
qelse g3(x,f g4(x,f g5 x))%1.

({eq d4}) and ({eq d5}) then give

!!d8:	%2∀x y.[y = f x ≡ ∃w.[y = α(w,x) ∧ ∀x.[x εε w ≡
.nofill
α(w,x) = qif p1 x qthen g1 x qelse qif p2(x,α(w,h1 x)) qthen g2 x qelse g3(x,α(w,g4(x,α(w,g5 x))))]]]%1.
.fill
%1
	⊗w, which we will call a %2pair-list%1 of ⊗f,
is a list of (argument.value) pairs for the function ⊗f, and
the second line of ({eq d8}) is obtained by replacing ⊗f(z) by ⊗α(w,z) 
everywhere it occurs in the recursive definition ({eq d7}).  We could
make the notation even more parallel by the syntactic sugar of writing
⊗f' instead of ⊗w and writing %2f'%8<%2z%8>%1 in place of ⊗α(w,x). 
This might well be justified since ⊗w can be regarded as a kind of
finite approximation of the graph of ⊗f that for every (argument.value)
pair it contains, also contains all pairs that come up in its evaluation.
The approximations %AW%1, %2F(%AW%1), %2F(F(%AW%1)), etc. are similar,
but since they include all pairs whose evaluation involves no more than
a certain number of recursions, ordinarily involve an infinite number
of pairs.

	Representing ⊗f by such a sentence characterizing %2pair-lists%1
avoids prescribing an order of evaluation
of terms.  There should be a Church-Rosser type theorem to the effect
that the value of ⊗f(x) is independent of the %2pair-list%1 used.
The use of %2pair-lists%1 rather than computation sequences enabled
us to write the representation of %2Y(F)%1 in terms of %2F%1.  Since
the computation sequence does not depend just on ⊗F we could not write
so simply a representation involving computation sequences.

	However, computation sequences are useful for analyzing time
taken and space used, and here is an approach to formalizing them.
Consider a recursive definition of the form

!!d9:	%2f x ← f1 m x

!!d10:	%2f1 y ← qif p y qthen g y qelse f h y%1.

	Such an ⊗f has a definite computation sequence determined
by ⊗p, ⊗g, and ⊗h, and any recursive function can be put into this
form in a variety of ways.  Each such way determines a computation
sequence.
.skip 2
.bb "#. Discussion"

	Many of the statements in this draft are tentative,
because I have not yet sufficiently understood work
by Cooper, Park, Igarashi, and Cartwright that may be relevant -
not to speak of results of recursive function theory.

	Cooper has shown that many statements about computer
programs such as their strong equivalence and termination or
non-termination can be formulated in second order logic.  Work
of Luckham, Park and Paterson has shown that the equivalence of
program schemata cannot be expressed as the validity or satisfiability
of a sentence of first order logic.  Therefore, it would seem
that equivalence of computer programs has been shown to require
second order logic.

	However, these results, while true, are somewhat misleading.  It
seems that equivalence, termination and many other properties of computer
programs are %2essentially%1 first order matters after all.  The situation
is analogous to that of Peano arithmetic.  First order arithmetic with an
axiom schema of induction is is incomplete and admits non-standard models.
Goedel's theorem shows that it cannot be completely axiomatized within any
logic that is complete such as first order logic.  Nevertheless, the
non-standard models are very weird and satisfy almost all the same
formulas as the standard models, so that all ordinary elementary theorems
of arithmetic can be proved within the first order system.  It should be
remarked that unadorned Peano arithmetic can express the mildly
set-theoretic arguments of informal arithmetic only at the cost of
encoding hereditarily finite sets built up from numbers by numbers.  The
system Z2 of (Cohen 1963) can express these arguments more directly, but
as Cohen shows, any theorem provable in Z2 can be proved in Peano
arithmetic at the cost of the encoding.  In a system like first order
formalized Lisp, the arguments involving finite sets can be made more
directly, because encoding sets of lists as lists is more straightforward
than encoding sets of integers as integers.
.skip 1
.begin verbatim
John McCarthy
Artificial Intelligence Laboratory
Computer Science Department
Stanford University
Stanford, California 94305

ARPANET: MCCARTHY@SU-AI
.end

.turn on "{"
%7This draft of
FIRST[W77,JMC]
PUBbed at {time} on {date}.%1